es:ES, L:(Id List).
fischer(L)
 (e:E, j:Id.
 Newround(e)  (j  L)  ((j = loc(e)))  (loc(the rcv(free message from e to j)) = j)) 

latex

Definitions	P & Q, source(l), destination(l), t  T, "$x", Id, <a, b>, x:A. B(x), loc(e), x:A  B(x), IdLnk, P  Q, the rcv(free message from e1 to j), ES, type List, fischer(L), t.1, E, Atom$n, Newround(e), x:A. B(x), (x  l), A, s = t, let x,y = A in B(x;y), {T}, b, !Void(), x:AB(x), False, A c B,
Lemmas	not wf, l member wf, f-newround wf, es-E wf, fischer wf, Id wf, event system wf, kind-f-free, es-kind-rcv, es-loc-pred, es-loc-rcv, f-free wf, es-loc wf